1. Field of the Invention
This invention pertains in general to Boolean satisfiability algorithms and in particular to an improvement in the searching steps inherent in such algorithms.
2. Description of Related Art
The last few years bave seen extraordinary improvements in the effectiveness of general-purpose Boolean satisfiability (SAT) algorithms. This work began with the application of the Walk-SAT (WSAT) algorithm to xe2x80x9cpracticalxe2x80x9d problems in a variety of domains, such as generative planning and circuit layout, by translating the problems into propositional logic and then solving them using WSAT.
Although WSAT is unchallenged in its ability to find models for randomly generated satisfiable theories, systematic methods have closed the gap on theories corresponding to practical problems. The algorithm of choice appears to be Relevance-bounded Learning (RELSAT), an extension of an idea from dynamic backtracking. RELSAT is systematic and can therefore deal with both satisfiable and unsatisfiable theories; for theories arising from practical problems, its performance is comparable to that of WSAT.
The applicability of propositional algorithms to practical problems is anything but straightforward, however. As the problems become more interesting, the problems"" sizes grow enormously due primarily to occurrences of constraint axioms containing universally quantified parameters. A single axiom such as
∀xyz. [a(x,y)xcex9b(y,z)xe2x86x92c(x,z)]xe2x80x83xe2x80x83(1)
has d3 ground instances if d is the size of the domain from which x, y and z are taken. The prior art has dealt with this difficulty by increasing computer memory and by finding clever axiomatizatidns for which ground theories remain manageably sized. In general, memory and cleverness are both scarce resources and a more natural solution is desired.
The above needs are met by a method, computer program product, and computer system for using a procedure, such as a search procedure, to solve a constraint problem. The method, computer program product, and computer system, according to embodiments of the present invention, define a set of constraints for the constraint problem. The set of constraints includes one or more lifted constraints with universally quantified parameters. The procedure is formulated in terms of subsearch problems on the one or more lifted constraints. A search procedure, such as WSAT or Davis-Putnam, searches for a satisfying assignment and encounters the subsearch problems. Then, intelligent subsearch is used to answer the subsearch problems. Intelligent subsearch includes using backtracking searches to find relevant assignments to the universally quantified parameters within the one or more lifted constraints. One embodiment of the present invention performs intelligent subsearch on each lifted constraint and merges the results. From the results of the intelligent subsearch, it is possible to supply the information needed by the search procedure to make its decisions. The goal of the search procedure is to find an assignment Q satisfying the defined set of constraints.
One embodiment of the present invention formulates the search procedure in terms of subsearch problems on S(C,P,u,s), where S(C,P,u,s) represents a subset of grounded clauses that would be obtained by grounding a set of clauses C obtained from the defined set of constraints for the constraint problem and restricting the subset of clauses having u literals unvalued by an assignment P and s literals satisfied by the assignment P. In alternative embodiments, C can be the set of one or more lifted clauses, a set of clauses in a set of possibly lifted clauses produced using a literal 1, clauses learned by a search procedure, and clauses learned by the search procedure and restricted using a literal l.
In one embodiment of the present invention, at least one lifted constraint is a pseudo-Boolean constraint.